a:. atomic(a)  prime(a) 

latex

Definitions	P  Q, P & Q, P  Q, {T}, atomic(a), x:A. B(x), t  T, prime(a), P  Q, A, False, b | a, gcd(a;b), P  Q, CoPrime(a,b), GCD(a;b;y), a ~ b
Lemmas	gcd is divisor 2, assoced inversion, divides functionality wrt assoced, assoced weakening, divides weakening, coprime prod, coprime elim a, gcd wf, gcd is divisor 1, divides wf, atomic wf, atomic char